[SOLVED] How does dafny prove this induction on maps?

I wrote a specification for the leetcode isomorphic strings problem based on the following TypeScript code. Basically, the approach is to assign each letter a number based on when it was first encountered, we do this for both strings and if the mapped strings are equivalent then they are isomorphic.

I interpret this to mean that there exists a function/mapping from string s to t, which is injective.

function isIsomorphic(s: string, t: string): boolean {

    let sMap = new Map<string, number>();
    let sTransform: number[] = [];
    let tMap = new Map<string, number>();
    let tTransform: number[] = [];
    
    let sIndex = 1;
    let tIndex = 1;
    if(s.length != t.length) return false
    
    for(let i = 0; i < s.length; i++) {
        if(!sMap.has(s[i])) {
            sMap.set(s[i], sIndex++);
        }
        sTransform.push(sMap.get(s[i])); 
    }
    
    for(let i = 0; i < t.length; i++) {
        if(!tMap.has(t[i])) {
            tMap.set(t[i], tIndex++);
        }
        tTransform.push(tMap.get(t[i])); 
    }
    
    return sTransform.every((elem, index) => elem == tTransform[index]);
};

My purpose in verifying the problem is to make my intuition explicit and formalize it so I actually understand the solution completely. I wrote this specification and it verifies but I still do not feel like I fully understand the specification because of Dafny's powerful induction ability. I feel like I haven't quite proved the relationship I was trying to formalize.

Helper functions:

predicate InjectiveMap<T,U>(f: map<T, U>)
{
    forall x, y :: x in f && y in f && x != y ==> f[x] != f[y]
}

//Apply a map to a sequence
function method aps<T,U>(s: seq<T>, smap: map<T,U>): seq<U>
    requires forall x :: x in s ==> x in smap
{
    seq(|s|, i requires 0 <= i < |s| => smap[s[i]])
}


function intsLessThan(n: nat): set<nat>
    ensures intsLessThan(n) == set x | 0 <= x < n
{
    if n == 0 then {} else {n-1} + intsLessThan(n-1)
}

function createMap(lmap: map<char,nat>, rmap: map<char, nat>): map<char, char>
    requires InjectiveMap(lmap)
    requires InjectiveMap(rmap)
    requires rmap.Values == lmap.Values
    ensures forall x :: x in lmap ==> x in createMap(lmap, rmap)
    ensures InjectiveMap(createMap(lmap, rmap))
{
    map xs : char | xs in lmap :: injectiveMapHasKey(rmap, lmap[xs]); var rkey :| rkey in rmap && rmap[rkey] == lmap[xs]; rkey
}

lemma injectiveMapHasKey<T,U>(lmap: map<T, U>, value: U)
    requires InjectiveMap(lmap)
    requires value in lmap.Values
    ensures exists t :: t in lmap && lmap[t] == value
{

}

The implementation only asserts that if answer is true then the implicit function/map which describes the isomorphism between the two strings exists. It feels like it should be a bi-conditional, but I feel less certain of how to prove that.

method isIsomorphic(s: string, t: string) returns (answer: bool) 
    requires 1 <= |s|
    requires |t| == |s|
    // ensures answer ==> exists fn: (char) -> char :: Injective(fn) && forall i :: 1 <= i < |s| <= |t| ==> fn(s[i]) == t[i]
    ensures answer ==> exists fn: map<char,char> :: InjectiveMap(fn) && forall i :: 1 <= i < |s| <= |t| ==> s[i] in fn && fn[s[i]] == t[i]
{
    var sMap: map<char, nat> := map[];
    var sTransform: seq<nat> := [];

    var tMap: map<char, nat> := map[];
    var tTransform: seq<nat> := [];

    var sIndex: nat := 0;
    // ghost var gsIndex: nat := 0;
    ghost var sIndices: set<nat> := {};
    var tIndex: nat := 0;
    for i := 0 to |s| 
        invariant forall j :: 0 <= j < i ==> s[j] in sMap
        invariant sIndices == intsLessThan(sIndex)
        invariant sIndex == |sMap|
        invariant sMap.Values == sIndices
        invariant InjectiveMap(sMap)
        invariant sTransform == aps(s[0..i], sMap)
    {
        if s[i] !in sMap {
            ghost var oldsMap := sMap;
            assert sIndex !in sIndices;
            assert sIndex !in sMap.Values;
            sMap := sMap[s[i] := sIndex];
            assert sMap == oldsMap + map[s[i] := sIndex];

            // assert forall z :: z in sMap && z != s[i] ==> sMap[z] != sIndex;
            sIndices := sIndices + {sIndex};
            assert sIndex in sMap.Values && sIndex in sIndices;
            sIndex := sIndex + 1;
        }
        sTransform := sTransform + [sMap[s[i]]];
    }
    
    ghost var tIndices: set<nat> := {};
    for i := 0 to |t| 
        invariant forall j :: 0 <= j < i ==> t[j] in tMap
        invariant tIndices == intsLessThan(tIndex)
        invariant tIndex == |tMap|
        invariant tMap.Values == tIndices
        invariant InjectiveMap(tMap)
        invariant tTransform == aps(t[0..i], tMap)
    {
        if t[i] !in tMap {
            ghost var tOld := tMap;
            assert tIndex !in tIndices;
            assert tIndex !in tMap.Values;
            tMap := tMap[(t[i]) := tIndex];
            assert tMap == tOld + map[t[i] := tIndex];
            tIndices := tIndices + {tIndex};
            assert tIndex in tMap.Values && tIndex in tIndices;
            tIndex := tIndex + 1;
        }
        tTransform := tTransform + [tMap[t[i]]];
    }
    assert sTransform == aps(s, sMap);
    assert tTransform == aps(t, tMap);
    if sMap.Values == tMap.Values && sTransform == tTransform {
        injectiveMapCanBeMade(sMap, tMap, s, t, sTransform, tTransform);
        return true;
    }else{
        return false;
    }
}

My question really lies in the lemmas, particularly createMapHasAllTheValues. To prove that the composite map of the map of the first string and map of the second string, can be used to map over the first string to recreate the second string, I thought I would have to make the relationships between the string s and t and their mapped version smapped and tmapped more explicit to actually show that applying the composite map to the values s[i] is equal to t[i], because nothing in post conditions of createMap (which creates the composite map), actually directly asserts anything about any positional value in s[i] or t[i].

What is it actually inducing on? How does assert smapped[i] == tmapped[i] imply createMap(lmap, rmap)[s[i]] == t[i]?

lemma injectiveMapCanBeMade(lmap: map<char,nat>, rmap: map<char, nat>, s: string, t: string, smapped: seq<nat>, tmapped: seq<nat>)
    requires InjectiveMap(lmap)
    requires InjectiveMap(rmap)
    requires rmap.Values == lmap.Values
    requires |s| == |t| && |s| >= 1
    requires forall i :: 0 <= i < |s| ==> s[i] in lmap
    requires forall i :: 0 <= i < |t| ==> t[i] in rmap
    requires smapped == aps(s, lmap)
    requires tmapped == aps(t, rmap)
    requires smapped == tmapped
    ensures exists fn: map<char,char> :: InjectiveMap(fn) && forall i :: 1 <= i < |s| <= |t| ==> s[i] in fn && fn[s[i]] == t[i]
{
    var fn := createMap(lmap, rmap);
    assert InjectiveMap(fn);
    createMapHasAllTheValues(lmap, rmap, s, t, smapped, tmapped);
}

lemma createMapHasAllTheValues(lmap: map<char,nat>, rmap: map<char, nat>, s: string, t: string, smapped: seq<nat>, tmapped: seq<nat>)
    requires InjectiveMap(lmap)
    requires InjectiveMap(rmap)
    requires forall j :: 0 <= j < |s| ==> s[j] in lmap
    requires forall j :: 0 <= j < |t| ==> t[j] in rmap
    requires smapped == aps(s, lmap)
    requires tmapped == aps(t, rmap)
    requires smapped == tmapped
    requires rmap.Values == lmap.Values
    ensures createMap(lmap, rmap).Values == rmap.Keys
    ensures forall i :: 0 <= i < |s| ==> createMap(lmap, rmap)[s[i]] == t[i]
{
    var test_map := createMap(lmap, rmap);
    assert createMap(lmap, rmap).Keys == lmap.Keys;
    forall x | x in rmap.Keys 
        ensures x in createMap(lmap, rmap).Values
    {
        assert rmap[x] in lmap.Values;
    }

    forall i | 0 <= i < |s|
        ensures createMap(lmap, rmap)[s[i]] == t[i]
    {
        // Why/How does the following prove the ensure?
        assert smapped[i] == tmapped[i];
    }

}

aside: I also notice just now that the method should actually assert that there exist two maps, one from s to t and another t to s, to really assert there is an isomorphism.